\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$).
\\[0ex]@loc($e$) discrete ${\it ds}$
\\[0ex]$\Rightarrow$ \=($\forall$$t$:rationals. \+
\\[0ex]es{-}state{-}after{-}elapsed(${\it es}$; $e$; $t$) = es{-}state{-}after(${\it es}$; $e$) $\in$ decl{-}state(${\it ds}$))
\-
\end{tabbing}